Nuprl Lemma : fun_exp_wf
11,40
postcript
pdf
T
:Type,
n
:
,
f
:(
T
T
).
f
^
n
T
T
latex
Definitions
f
^
n
,
t
T
,
x
:
A
.
B
(
x
)
,
Lemmas
nat
wf
,
int
seg
wf
,
compose
wf
,
primrec
wf
origin